Inference at * 1 1 2 2 
Iof proof for Lemma complete nat ind with y:



1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
3. Y(f,x. g(x,f))  !Void()!Void()
4. n:. Y(f,x. g(x,f))  (m:n. P(m))
  Y(f,x. g(x,f))  (i:. P(i)) 

latex

 by ((ExtWith [`r'] [!Void()!Void()]) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 5. r : 
C1:   Y((f,x. g(x,f)),r)  P(r)
C.

Definitions	t  T, x:A. B(x)
Lemmas	nat wf